$\forall$${\it the\_es}$:ES, ${\it e'}$:E, $l$:IdLnk, $n$:\{0..($\parallel$sends($l$;${\it e'}$)$\parallel$+1)$^{-}$\}, $m$:Msg.
\\[0ex]($m$ $\in$ snds($l$, before(${\it e'}$,$n$)))
\\[0ex]$\Leftarrow\!\Rightarrow$ (($\exists$$e$:E. (($e$ $<$loc ${\it e'}$) \& ($m$ $\in$ sends($l$;$e$)))) $\vee$ ($\exists$$i$:\{0..$n$$^{-}$\}. ($m$ = sends($l$;${\it e'}$)[$i$])))